$\forall$${\it the\_w}$:World, $i$:Id. MsgFrom($i$) $\in$ Type